1. Field of the Invention
The present invention relates generally to an improved formal verification system, and more specifically to formal verification of bounded fairness properties of pseudo random number generators and arbiters that use random priority based arbitration schemes.
2. Description of the Related Art
Electronic systems such as microprocessors and peripheral chips extensively use arbiters. The primary function of an arbiter is to restrict the number of concurrent accesses to a shared resource. A variety of arbitration schemes employed by arbiters serialize the access requests to the shared resource whenever there are more number of requests than the constant number of concurrent requests a shared resource can satisfy.
Processors use arbitration logic in several places, such as in the logic used for controlling the access to cache directories and shared buses. The commonly used arbitration schemes assign a priority to the input requests and grant the highest priority requests before other pending or concurrent low priority requests. The basis for the priority assignment may be either a fixed priority scheme (e.g., request i always gets higher priority than request j) or a dynamic priority scheme. Dynamic priority schemes include one based on the relative arrival time of the requests (e.g. first in, first out (FIFO)), one based on a strict rotation of priority assignments to the requests (e.g. round-robin), or one based on assigning a random priority to the incoming requests (e.g., pseudo random number generator). An example of a pseudo random number generator is a Linear Feedback Shift Register (LFSR). Regardless of the arbitration scheme used, it is important to specify and verify the desired fairness properties of the arbitration scheme. Fairness ensures that all requests are given equal opportunity to be granted and that no requests are forced to starve. Formal verification techniques may verify and prove that the arbitration logic is starvation free (i.e., the arbitration logic does not starve any requests indefinitely or beyond a certain number of cycles) under the specified fairness conditions.